Nuprl Lemma : no_repeats_member
0,22
postcript
pdf
T
:Type,
L
:
T
List,
x
:
T
. no_repeats(
T
;
L
)
(
x
L
)
(
x
!
L
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
no_repeats(
T
;
l
)
,
(
x
l
)
,
(
x
!
l
)
,
P
Q
,
False
,
A
,
A
B
,
,
A
&
B
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Prop
,
{
T
}
,
P
Q
,
P
Q
,
P
Q
Lemmas
cons
member
,
cons
member!
,
no
repeats
cons
,
l
member!
wf
,
not
wf
,
l
member
wf
,
no
repeats
wf
origin
T:Type, L:T List, x:T. no_repeats(T;L) 
(x 
L) (x ! L) T:Type, L:T List, x:T. no_repeats(T;L) (x L) (x ! L) Tx:A. B(x) l)! l) Q
A
B
x:A. B(x)
Q
Q Q